package controller.solver;

import java.io.IOException;
import java.util.concurrent.Semaphore;

import model.solver.SolverResult;
import model.solver.SolverResultStatus;
import controller.OutputReader;

/**
 * 
 * <p>
 * This Class provide a model for you to add and implement your own solver. It take care of the
 * maximum of operation so that you only need the give the minimum amount of information and add as
 * quickly as possible your solver.
 * </p>
 * <p>
 * So to add your solver you only need to implement the hasTimeout method, return false if your
 * solver has no timeout, getCommandLine that return the command line that should be run and also
 * checkParameter that check if everything is fine with the parameter (I recommend to create a new
 * Parameter Class). It also provide you a way to to some additional work after the execution by
 * implementing the returnXXXX method that are call after the execution return the XXXX status. Be
 * aware of the returnProblemCNF method.
 * </p>
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public abstract class SolverModel extends Solver {

	/** The default value that is associate to a UNSATISFIABLE result */
	public static final int	RETURN_UNSATISFIABLE	= 20;
	/** The default value that is associate to a SATISFIABLE result */
	public static final int	RETURN_SATISFIABLE		= 10;
	/** The default value that is associate to a UNKNOWN result */
	public static final int	RETURN_UNKNOWN			= -10;

	protected int			returnSat				= RETURN_SATISFIABLE;
	protected int			returnUnSat				= RETURN_UNSATISFIABLE;
	protected int			returnUnknown			= RETURN_UNKNOWN;
	protected String		description;

	/**
	 * Create a {@link SolverModel}.
	 * 
	 * @param description
	 *            Description of the solver
	 * @param sat
	 *            value that is return by the solver when the result is SATISFIABLE
	 * @param unsat
	 *            value that is return by the solver when the result is UNSATISFIABLE
	 */
	public SolverModel(String description, int sat, int unsat) {
		returnSat = sat;
		returnUnSat = unsat;
		this.description = description;
	}

	@Override
	public SolverResult runSolver(String[] cmd, Semaphore manager) {
		SolverResult res = new SolverResult();
		res.setStatus(SolverResultStatus.UNKNOWN);

		OutputReader outreader = null;
		OutputReader errreader = null;
		Thread tout = null;
		Thread terr = null;
		try
		{// lance le processus
			res.setBegin(System.currentTimeMillis());
			setRunning(true);

			try
			{
				process = Runtime.getRuntime().exec(cmd);
			} catch (IOException e)
			{
				throw e;
			}
			finally
			{// libere les sem
				sem.release();
				if (manager != null)
					manager.release();
			}

			outreader = new OutputReader(process.getInputStream(), res, false);
			errreader = new OutputReader(process.getErrorStream(), res, true);
			tout = new Thread(outreader);
			tout.start();
			terr = new Thread(errreader);
			terr.start();
		} catch (IOException e)
		{
			e.printStackTrace();
			res.setStatus(SolverResultStatus.PROBLEM);
			if (process != null)
				process.destroy();
		}

		finally
		{
			try
			{
				if (process != null)
					res.setExitVal(process.waitFor());

				if (tout != null)
					tout.join();
				if (terr != null)
					terr.join();

				if (outreader != null && outreader.getReturnValue() != OutputReader.DEFAULT_RETURN_VALUE)
					throw new IOException("problem stdout solver model");
				if (errreader != null && errreader.getReturnValue() != OutputReader.DEFAULT_RETURN_VALUE)
					throw new IOException("problem stderr solver model");
			} catch (Exception e)
			{
				e.printStackTrace();
				res.setStatus(SolverResultStatus.PROBLEM);
			}
			finally
			{
				try
				{
					sem.acquire();
				} catch (InterruptedException e)
				{
					e.printStackTrace();
					return null;
				}

				setRunning(false);
			}
		}
		// terminer
		res.setEnd(System.currentTimeMillis());

		// System.out.println("val de retour"+res.getExitVal());

		// dernier details
		res.setDescription(description);

		// s'occupe du status
		if (hasBeenStop())
		{// cas stop
			res.setStatus(SolverResultStatus.STOP);
			returnHasBeenStop(res);
		}
		else
			if (hasBeenTimeout())
			{// cas timeout
				res.setStatus(SolverResultStatus.TIMEOUT_REACHED);
				returnHasBeenTimeout(res);
			}
			else
				if (res.getStatus() == SolverResultStatus.PROBLEM)
				{
					res.setStatus(SolverResultStatus.PROBLEM);
					returnProblem(res);
				}
				else
					if (res.getExitVal() == returnUnSat)
					{// UNSAT
						res.setStatus(SolverResultStatus.UNSATISFIABLE);
						returnUnSat(res);
					}
					else
						if (res.getExitVal() == returnSat)
						{ // SAT
							res.setStatus(SolverResultStatus.SATISFIABLE);
							returnSat(res);
						}
						else
						{ // UNKNOWN
							res.setStatus(SolverResultStatus.UNKNOWN);
							returnUnknown(res);
						}


		// libere le sem
		sem.release();

		return res;
	}

	@Override
	public abstract boolean hasTimeout();

	/**
	 * Is call when the result after the execution of the solver is SAT.
	 * 
	 * @param res
	 *            the actual result of the solving
	 */
	protected abstract void returnSat(SolverResult res);

	/**
	 * Is call when the result after the execution of the solver is UNSAT.
	 * 
	 * @param res
	 *            the actual result of the solving
	 */
	protected abstract void returnUnSat(SolverResult res);

	/**
	 * Is call when the result after the execution of the solver is UNKNOWN.
	 * 
	 * @param res
	 *            the actual result of the solving
	 */
	protected abstract void returnUnknown(SolverResult res);

	/**
	 * Is call when there was a problem.
	 * 
	 * @param res
	 *            the actual result of the solving
	 */
	protected abstract void returnProblem(SolverResult res);

	/**
	 * Is call after the execution of the solver has been stop by the timeout.
	 * 
	 * @param res
	 *            the actual result of the solving
	 */
	protected abstract void returnHasBeenTimeout(SolverResult res);

	/**
	 * Is call after the execution of the solver has been stop.
	 * 
	 * @param res
	 *            the actual result of the solving
	 */
	protected abstract void returnHasBeenStop(SolverResult res);

	@Override
	public abstract String[] getCommandLine(String cnfFile);

}
